(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_LRA)
(declare-fun v0 () Real)
(assert (let ((e1 7))
(let ((e2 6))
(let ((e3 (/ e1 (- e2))))
(let ((e4 (* e1 v0)))
(let ((e5 (distinct v0 v0)))
(let ((e6 (= e3 e4)))
(let ((e7 (ite e5 e4 v0)))
(let ((e8 (ite e6 v0 e7)))
(let ((e9 (ite e6 e8 e4)))
(let ((e10 (ite e5 e3 e8)))
(let ((e11 (distinct e8 v0)))
(let ((e12 (>= e10 e7)))
(let ((e13 (= e7 v0)))
(let ((e14 (distinct e9 e3)))
(let ((e15 (= e3 e4)))
(let ((e16 (= e14 e12)))
(let ((e17 (and e16 e13)))
(let ((e18 (= e6 e5)))
(let ((e19 (not e17)))
(let ((e20 (=> e18 e19)))
(let ((e21 (ite e15 e20 e11)))
e21
))))))))))))))))))))))

(check-sat)
